Add Erdős Problem 1167 (stepping-down partition relation)#3791
Add Erdős Problem 1167 (stepping-down partition relation)#3791henrykmichalewski wants to merge 3 commits into
Conversation
Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.
Paul-Lez
added
the
awaiting-author
mo271
removed
the
awaiting-author
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Nice formalization — CardinalPartitionRel is a clean definition that captures the partition arrow well, and the translation is faithful. A few issues:
- Excessive docstring duplication
The problem statement appears ~4 times: the verbatim quote (line 23), the "Problem Statement" section (lines 34–38), the overview paraphrase (lines 57–59), and the erdos_1167 theorem docstring (lines 105–118). Per project conventions, the problem text should appear only once. Please keep the verbatim quote in the module docstring and trim the rest — the theorem docstring should describe anything not already in the module docstring rather than restating it.
- Non-standard module docstring format
The module docstring uses non-standard headers: Verbatim statement (Erdős #1167, status O):, Source:, Notes: OPEN. Please use the standard format with just Reference: and the verbatim quote.
- CardinalPartitionRel should be in ForMathlib
This is a clean, general definition of the partition arrow
- binary_colors variant doesn't use CardinalPartitionRel
All other variants reuse CardinalPartitionRel, but binary_colors inlines the definition manually with Fin 2 and a disjunction (∨). This creates code duplication and inconsistency. Please rewrite it using CardinalPartitionRel with γ = 2.
- Missing answer(sorry)
The source asks "Is it true that...?" — a yes/no question. Per project conventions this should use answer(sorry) ↔ ∀ (r : ℕ), 2 ≤ r → .... The current formulation asserts the statement directly, which presupposes the answer is "yes."
- Sanity checks don't test CardinalPartitionRel
The current tests (ℵ₀ ≤ ℵ₀, ℵ₀ < 2^ℵ₀, s.card = 0 → s = ∅) are trivial facts that don't exercise the central definition at all. Consider adding tests that actually involve CardinalPartitionRel, e.g. the trivial/vacuous cases or a known finite Ramsey instance.
| /-- | ||
| **Sanity check**: The hypothesis `ℵ₀ ≤ lam` is non-vacuous: $\aleph_0$ is an infinite cardinal. | ||
| -/ | ||
| @[category test, AMS 5] | ||
| example : ℵ₀ ≤ ℵ₀ := le_refl _ | ||
|
|
||
| /-- | ||
| **Sanity check**: $2^{\aleph_0} > \aleph_0$, so the power $2^\lambda$ is strictly larger than | ||
| $\lambda$ for $\lambda = \aleph_0$. This confirms the two base sets in the stepping-down | ||
| implication are genuinely of different sizes. | ||
| -/ | ||
| @[category test, AMS 5] | ||
| example : ℵ₀ < (2 : Cardinal) ^ ℵ₀ := Cardinal.cantor ℵ₀ | ||
|
|
||
| /-- | ||
| **Sanity check**: Every 0-element finset is empty. This confirms `Finset.card = 0` is | ||
| non-trivial and that the condition `s.card = r` in `CardinalPartitionRel` correctly captures | ||
| the notion of an $r$-element subset. | ||
| -/ | ||
| @[category test, AMS 5] | ||
| example (A : Type u) (s : Finset A) (hs : s.card = 0) : s = ∅ := | ||
| Finset.card_eq_zero.mp hs |
There was a problem hiding this comment.
none of these are really useful: they are just some theorems in mathlib that don't need repeating here -- those definitions are sufficiently tested in mathlib
Per mo271 review on PR google-deepmind#3791 — 6 issues + 1 inline: 1. Statement deduplication — kept only the verbatim quote in the erdos_1167 theorem docstring; removed the ## Problem Statement / ## Overview / theorem-body restatement bloat. 2. Module docstring standardised — now just *Reference:* + brief formalisation notes; dropped the **Verbatim statement** / **Source** / **Notes: OPEN** non-standard headers. 3. CardinalPartitionRel factored into FormalConjecturesForMathlib — new module FormalConjecturesForMathlib/Combinatorics/SetTheory/PartitionRelation.lean defines Combinatorics.cardinalPartitionRel with the same signature; added to the umbrella import. The local Erdos1167.CardinalPartitionRel is gone. 4. binary_colors variant rewritten to use cardinalPartitionRel with γ = 2 (instantiating the type-uniformly via ((2 : Ordinal.{u}).ToType → Cardinal)). Was previously inlined as a Fin 2-valued disjunction. 5. erdos_1167 now uses the answer(sorry) ↔ ... pattern (was previously asserting the implication directly, presupposing the answer is yes). 6. Trivial sanity checks dropped — the three tests (ℵ₀ ≤ ℵ₀, ℵ₀ < 2^ℵ₀, s.card = 0 → s = ∅) were Mathlib facts that didn't exercise the central definition, per mo271's inline at line 247. Builds cleanly: lake build FormalConjectures.ErdosProblems.«1167» Net diff on 1167.lean: -134 / +30 (substantially shorter, focused).
|
@mo271 — applied all 6 issues + your inline comment in
Net diff on |
|
Thanks! Some more review comments:
The module docstring (lines 24–35) contains a "Formalization notes" section explaining implementation choices (Ordinal.ToType, avoiding λ, cardinal successor). The module docstring should contain only the title and reference — not formalization notes. The last bullet about
The PartitionRelation.lean file is clean (no sorry, correct conventions), but it only contains the bare definition. Even one or two sorry-free lemmas would improve reusability — e.g., the trivial 0-uniform case, or monotonicity in the source cardinal.
Consider adding @[category test] sanity checks that exercise cardinalPartitionRel — the old trivial tests (ℵ₀ ≤ ℵ₀, s.card = 0 → s = ∅) were correctly removed but not replaced.
|
mo271
added
the
awaiting-author
3 participants
Formalizes Erdős Problem 1167 concerning a stepping-down partition relation for cardinals.
Contents
CardinalPartitionRel μ r γ ν: anr-uniform generalization of the cardinal partition relationμ → (ν)^r_γ, asserting that for every coloring ofr-element subsets ofμwithγcolors there is a monochromatic subset of sizeν.finite_targets: behavior with finite target cardinalitiesbinary_colors: the two-color specializationinfinite_targets: behavior for infinite targetsr_eq_two: ther = 2(graph) specializationCloses #1991
Assisted by Claude (Anthropic).